Left Termination of the query pattern
bin_tree_in_1(g)
w.r.t. the given Prolog program could successfully be proven:
↳ Prolog
↳ PrologToPiTRSProof
Clauses:
bin_tree(void).
bin_tree(tree(X, Left, Right)) :- ','(bin_tree(Left), bin_tree(Right)).
Queries:
bin_tree(g).
We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
bin_tree_in(tree(X, Left, Right)) → U1(X, Left, Right, bin_tree_in(Left))
bin_tree_in(void) → bin_tree_out(void)
U1(X, Left, Right, bin_tree_out(Left)) → U2(X, Left, Right, bin_tree_in(Right))
U2(X, Left, Right, bin_tree_out(Right)) → bin_tree_out(tree(X, Left, Right))
The argument filtering Pi contains the following mapping:
bin_tree_in(x1) = bin_tree_in(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
U1(x1, x2, x3, x4) = U1(x3, x4)
void = void
bin_tree_out(x1) = bin_tree_out
U2(x1, x2, x3, x4) = U2(x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
Pi-finite rewrite system:
The TRS R consists of the following rules:
bin_tree_in(tree(X, Left, Right)) → U1(X, Left, Right, bin_tree_in(Left))
bin_tree_in(void) → bin_tree_out(void)
U1(X, Left, Right, bin_tree_out(Left)) → U2(X, Left, Right, bin_tree_in(Right))
U2(X, Left, Right, bin_tree_out(Right)) → bin_tree_out(tree(X, Left, Right))
The argument filtering Pi contains the following mapping:
bin_tree_in(x1) = bin_tree_in(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
U1(x1, x2, x3, x4) = U1(x3, x4)
void = void
bin_tree_out(x1) = bin_tree_out
U2(x1, x2, x3, x4) = U2(x4)
Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
BIN_TREE_IN(tree(X, Left, Right)) → U11(X, Left, Right, bin_tree_in(Left))
BIN_TREE_IN(tree(X, Left, Right)) → BIN_TREE_IN(Left)
U11(X, Left, Right, bin_tree_out(Left)) → U21(X, Left, Right, bin_tree_in(Right))
U11(X, Left, Right, bin_tree_out(Left)) → BIN_TREE_IN(Right)
The TRS R consists of the following rules:
bin_tree_in(tree(X, Left, Right)) → U1(X, Left, Right, bin_tree_in(Left))
bin_tree_in(void) → bin_tree_out(void)
U1(X, Left, Right, bin_tree_out(Left)) → U2(X, Left, Right, bin_tree_in(Right))
U2(X, Left, Right, bin_tree_out(Right)) → bin_tree_out(tree(X, Left, Right))
The argument filtering Pi contains the following mapping:
bin_tree_in(x1) = bin_tree_in(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
U1(x1, x2, x3, x4) = U1(x3, x4)
void = void
bin_tree_out(x1) = bin_tree_out
U2(x1, x2, x3, x4) = U2(x4)
BIN_TREE_IN(x1) = BIN_TREE_IN(x1)
U21(x1, x2, x3, x4) = U21(x4)
U11(x1, x2, x3, x4) = U11(x3, x4)
We have to consider all (P,R,Pi)-chains
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
Pi DP problem:
The TRS P consists of the following rules:
BIN_TREE_IN(tree(X, Left, Right)) → U11(X, Left, Right, bin_tree_in(Left))
BIN_TREE_IN(tree(X, Left, Right)) → BIN_TREE_IN(Left)
U11(X, Left, Right, bin_tree_out(Left)) → U21(X, Left, Right, bin_tree_in(Right))
U11(X, Left, Right, bin_tree_out(Left)) → BIN_TREE_IN(Right)
The TRS R consists of the following rules:
bin_tree_in(tree(X, Left, Right)) → U1(X, Left, Right, bin_tree_in(Left))
bin_tree_in(void) → bin_tree_out(void)
U1(X, Left, Right, bin_tree_out(Left)) → U2(X, Left, Right, bin_tree_in(Right))
U2(X, Left, Right, bin_tree_out(Right)) → bin_tree_out(tree(X, Left, Right))
The argument filtering Pi contains the following mapping:
bin_tree_in(x1) = bin_tree_in(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
U1(x1, x2, x3, x4) = U1(x3, x4)
void = void
bin_tree_out(x1) = bin_tree_out
U2(x1, x2, x3, x4) = U2(x4)
BIN_TREE_IN(x1) = BIN_TREE_IN(x1)
U21(x1, x2, x3, x4) = U21(x4)
U11(x1, x2, x3, x4) = U11(x3, x4)
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 1 less node.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ PiDPToQDPProof
Pi DP problem:
The TRS P consists of the following rules:
U11(X, Left, Right, bin_tree_out(Left)) → BIN_TREE_IN(Right)
BIN_TREE_IN(tree(X, Left, Right)) → U11(X, Left, Right, bin_tree_in(Left))
BIN_TREE_IN(tree(X, Left, Right)) → BIN_TREE_IN(Left)
The TRS R consists of the following rules:
bin_tree_in(tree(X, Left, Right)) → U1(X, Left, Right, bin_tree_in(Left))
bin_tree_in(void) → bin_tree_out(void)
U1(X, Left, Right, bin_tree_out(Left)) → U2(X, Left, Right, bin_tree_in(Right))
U2(X, Left, Right, bin_tree_out(Right)) → bin_tree_out(tree(X, Left, Right))
The argument filtering Pi contains the following mapping:
bin_tree_in(x1) = bin_tree_in(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
U1(x1, x2, x3, x4) = U1(x3, x4)
void = void
bin_tree_out(x1) = bin_tree_out
U2(x1, x2, x3, x4) = U2(x4)
BIN_TREE_IN(x1) = BIN_TREE_IN(x1)
U11(x1, x2, x3, x4) = U11(x3, x4)
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
BIN_TREE_IN(tree(X, Left, Right)) → U11(Right, bin_tree_in(Left))
BIN_TREE_IN(tree(X, Left, Right)) → BIN_TREE_IN(Left)
U11(Right, bin_tree_out) → BIN_TREE_IN(Right)
The TRS R consists of the following rules:
bin_tree_in(tree(X, Left, Right)) → U1(Right, bin_tree_in(Left))
bin_tree_in(void) → bin_tree_out
U1(Right, bin_tree_out) → U2(bin_tree_in(Right))
U2(bin_tree_out) → bin_tree_out
The set Q consists of the following terms:
bin_tree_in(x0)
U1(x0, x1)
U2(x0)
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- BIN_TREE_IN(tree(X, Left, Right)) → U11(Right, bin_tree_in(Left))
The graph contains the following edges 1 > 1
- BIN_TREE_IN(tree(X, Left, Right)) → BIN_TREE_IN(Left)
The graph contains the following edges 1 > 1
- U11(Right, bin_tree_out) → BIN_TREE_IN(Right)
The graph contains the following edges 1 >= 1